Inference at * 1 1 1 1 
Iof proof for Lemma complete nat ind with y:



1. P : {k}
2. g : i:. (j:i. P(j))  P(i)
  (x.g(x,Y(f,x. g(x,f))))  !Void()!Void() 

latex

 by ((MemCD) 
CollapseTHEN ((Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 3:n
C)) (first_tok :t) inil_term))) 

latex

C.

Definitions

t  T